b:, a:. u,v:. gcd_p(a; b; ((u * a) + (v * b))) 

latex

Definitions	, prop{i:l}, False, A, A  B, ge(i; j), P  Q, t  T, x:A. B(x), True, T, x:A. B(x), , P  Q, P  Q, P  Q, P  Q, decidable(P), lelt(i; j; k), int_seg(i; j)
Lemmas	le wf, ge wf, nat properties, nat wf, decidable int equal, true wf, squash wf, gcd p wf, gcd p zero, quot rem exists, gcd p sym, mul com, add functionality wrt eq, gcd p shift